1. Field of the Invention
The present invention generally relates to an automatic test pattern generation (ATPG) engine and, more particularly, to a method that quickly analyzes and efficiently models a new decision selection mechanism based on connectivity gates in a circuit for the purpose of computing all solutions for a target objective. Symmetry in search states is analyzed for success driven learning to reduce the number of backtraces incurred during the solution search. A new metric is implemented for determining the use of learned information for storage and later use. The invention has application in semiconductor design and manufacture as well as other design verification environments.
2. Background Description
In recent years, Automatic Test Pattern Generation (ATPG)/Boolean Satisfiability (SAT) based methods have offered a potential substitute for Reduced Ordered Binary Decision Diagrams (ROBDD) based methods. Unlike ROBDD based methods that can suffer from memory explosion, ATPG/SAT based methods can perform image or preimage computation with reduced memory requirements. Image/Preimage computation is performed by modifying the underlying ATPG algorithm, to generate all the available solutions, and it is a key step in sequential equivalence checking and unbounded model checking. In addition to design verification, ATPG engines that are able to generate multiple solutions can also be used to generate different and distinct multiple-detect test vectors for a given fault, thus improving the overall defect coverage of a test suite.
Traditionally, ATPG engines are guided by the testability measures of the circuit. Several heuristics have been developed to determine these measures that help to find any available solution quickly. The distance based testability measures account for the difficulty of testing a gate, based on its distance from the primary inputs and primary outputs. The 0/1 probability at the output of each gate in the circuit have been computed and used as testability measures. Certain numbers, called SCOAP measures, have been derived for each gate in the circuit, that represent the difficulty of justifying and propagating a value. All these testability measures guide the ATPG engine while backtracing from the objective to select a decision variable. Improvements to obtain better testability measures have been incorporated using the concept of super-gates. However, the worst-case complexity of obtaining these measures can he exponential. Recently, a better approximation for the testability measures has been obtained using implications generated in the circuit. Based on implication reasoning, a correlation factor that accounts for signal correlations in the circuit is estimated. However, all these testability measures aim at finding a single solution quickly. Likewise, in SAT, many variable/decision selection strategies have been proposed. such as MOMS (Maximum Occurences in clause of Minimum Size), DLIS (Dynamic Largest Individual Sum) and VSIDS (Variable State Independent Decaying Sum). However, these methods lack the structural information available to ATPG engines. SAT and ATPG have been integrated to develop an ATPG based SAT solver. The variable selection strategy of ATPG is used due to their superiority in choosing variables related to the objective.
“All-solutions ATPG” based methods have found applications in Model checking sequential circuits, and they can also improve the defect coverage of a test suite, by generating distinct multiple-detect patterns. Conventional decision selection heuristics and learning techniques for an ATPG engine were originally developed to quickly find any available (single) solution. Such decision solution heuristics may not be the best for an “all-solutions ATPG” engine, where all the solutions need to be found. In this paper, we explore new techniques to guide an “all-solutions ATPG engine.” An all-solutions ATPG attempts to build a complete decision tree (which can be reduced to a graph by sharing common sub-trees) that is essentially a Free Binary Decision Diagram (Free BDD). Conventionally, the testability measures of the circuit guide an ATPG engine to select decisions as they search for the solution. As a result, the variable order in the Free BDD conforms to the testability measures of the circuit. It is necessary to bias the variable order in such a way that we obtain a compact Free BDD as a whole. A compact Free BDD helps to reduce the size of the decision tree and in turn speeds up the ATPG engine. If the number of solutions in very large, in the order of billions, then it is not possible to store each solution oneby-one due to memory and time limitation. This phenomenon is referred to as solution explosion and it has been shown that the final solution-set can be efficiently represented by the decision tree as a Free BDD. Therefore it is necessary to obtain a compact Free BDD in order to address the solution explosion problem as well. Furthermore, as each ATPG decision leads to a different search-state in the decision tree, the number of search-states can be exponential in the number of inputs. Since each search-state is stored in a hash table, for use in success-driven learning, the memory required to store all of the search-states becomes a critical issue. Storing all the search-states in a knowledge-base may potentially lead to memory explosion for large circuits. In order to reduce the size of the knowledge-base and still benefit from useful search-states, it may be sufficient to store only the frequently occurring search-states.
Related work on BDD variable ordering and learning heuristics includes OBDD based methods that are very sensitive to their variable order and thus are limited to small and medium sized circuits. Significant amount of work has been done on finding an efficient variable ordering technique. Most of the work aims at placing related variables together in order to obtain a compact BDD. A PODEM based variable ordering technique has been considered for building ROBDDs. The testability measures of PODEM are used to back trace to the primary inputs by a depth-first search and the inputs connected by shorter paths are placed together. Recently, static variable ordering techniques have been proposed, and experimental results showed that these techniques can be better than dynamic variable ordering techniques. It is supposed that placing connected variables together and partitioning the variables lead to compact BDDs and faster SAT. On the other hand, Free BDDs (FBDDs) are relaxed versions of Ordered BDDs, in which variables can appear in different orders along different paths but each variable occurs only once along any given path. They are more compact than Ordered BDDs and sometimes lead to exponential savings in memory. Although significant amount of work has been done to develop good-variable ordering heuristics for ROBDDs, not much work has been done for Free BDDs.
In addition to variable selection heuristics, learning plays an important role in SAT/ATPG based methods. It helps to overcome the inherent time limitation of these methods and compete with BDD based methods. Powerful learning techniques have been introduced for ATPG. Efficient conflict-driven learning techniques have also been introduced for SAT based methods. Learning techniques have been proposed for an all-solutions SAT solver. These learning techniques improve the efficiency of the SAT solver that is an integral part of unbounded model checking. The strengths of both SAT & ATPG have been combined to provide efficient learning techniques for the sequential justification problem. It has also been proposed to provide signal correlation guided learning for an ATPG based SAT solver and obtained a speedup for hard industrial circuits. In all these aforementioned ATPG/SAT engines, the knowledge is in the form of implications, assertions or conflict clauses. Efficient manipulation of knowledge is required to reduce the overhead in storing and using the knowledge base.
Recently, a new type of “success-driven learning” that efficiently prunes the search-space for “ATPG based preimage computation” by identifying identical solution-subspaces has been introduced. The Transition Relation is represented by a levelized circuit and the set of states is stored in a Free BDD. A PODEM based ATPG engine is invoked to find all the solutions, resulting in a preimage where all the current state variables are quantified. Equivalent search-states that lead to the same solution subspace are identified to prune the search-space. The decision tree obtained during solution-search, is stored as a Free BDD that represents the complete preimage set. As solution subspaces heavily overlap during preimage computation, considerable savings is obtained in terms of time and memory. “Augmented success driven learning” and “search-state based conflict driven learning” have been introduced to further prune the search space for ATPG based preimage computation. However, conventional testability measures were used to guide the ATPG engine, resulting in suboptimal all-solutions FBDDs.